DECLARE INDCONST FOOL ε PERSON;

DECLARE INDVAR S S1 S2 S3 S4 ε PERSON;
DECLARE INDVAR W W1 W2 W3 ε WORLD;
DECLARE INDVAR P P1 P2 P3 P4 Q Q1 Q2 Q3 Q4 R R1 R2 R3 R4 ε PROPOSITION;

DECLARE OPCONST K(PERSON,PROPOSITION) = PROPOSITION;
DECLARE OPCONST KW(PERSON,PROPOSITION) = PROPOSITION;
DECLARE OPCONST AND(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST OR(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST IMP(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST EQUIV(PROPOSITION,PROPOSITION) = PROPOSITION;
DECLARE OPCONST NOT(PROPOSITION) = PROPOSITION;

DECLARE PREDCONST T(PROPOSITION,WORLD);
DECLARE PREDCONST A(PERSON,WORLD,WORLD);

AXIOM REFLEX: ∀ S W.(A(S,W,W));;

AXIOM KNOW: ∀ S P W.(T(K(S,P),W) ≡ ∀W1.(A(S,W,W1) ⊃ T(P,W1)));;

AXIOM KW: ∀ S P W.(T(KW(S,P),W) ≡ T(K(S,P),W) ∨ T(K(S,NOT(P)),W));;

AXIOM FOOL: ∀ S P W.(T(K(FOOL,P),W) ⊃ T(K(FOOL,K(S,P)),W));;

AXIOM AND: ∀ W P Q.(T(AND(P,Q),W) ≡ T(P,W) ∧ T(Q,W));;
AXIOM OR: ∀ W P Q.(T(OR(P,Q),W) ≡ T(P,W) ∨ T(Q,W));;
AXIOM IMP: ∀ W P Q.(T(IMP(P,Q),W) ≡ T(P,W) ⊃ T(Q,W));;
AXIOM EQUIV: ∀ W P Q.(T(EQUIV(P,Q),W) ≡ (T(P,W) ≡ T(Q,W)));;
AXIOM NOT: ∀ W P.(T(NOT(P),W) ≡ ¬T(P,W));;